\begin{tad}{CASILLA}
\\
\hrule

\generadores

  \alinearfuncs{Propiedad}{nat/valor}
    \func{Propiedad}{nat/valor}{casilla}{n mod 1000 = 0}
    \func{Carcel}{}{casilla}{}
    \func{Inicio}{}{casilla}{}

\observadores

  \alinearfuncs{esPropiedad?}{casilla/c}{bool}
	\func{esCarcel?}{casilla/c}{bool}{}
	\func{esPropiedad?}{casilla/c}{bool}{}
	\func{esInicio?}{casilla/c}{bool}{}
	\func{Valor}{casilla/c}{nat}{esPropiedad?(c)}{}

\axiomas{($\forall$ c:casilla, valor:nat)}
	\axioma{esCarcel?(Propiedad(x))}{false}
	\axioma{esCarcel?(Inicio)}{false}
	\axioma{esCarcel?(Carcel)}{true}
	\axioma{esInicio?(Propiedad(x))}{false}
	\axioma{esInicio?(Carcel)}{false}
	\axioma{esInicio?(Inicio)}{true}
	\axioma{esPropiedad?(Propiedad(x))}{true}
	\axioma{esPropiedad?(Carcel)}{false}
	\axioma{esPropiedad?(Inicio)}{false}
	\axioma{Valor(Propiedad(x))}{x}

\end{tad}
